package com.google.code.securityflow.datalog

import java.lang.StringBuilder
import com.google.code.securityflow.cfg._

object Facts {

  def build(flowGraph: FlowGraph): String = {
    val sb = new StringBuilder();
    val mainFunction = flowGraph.main;

    for (block <- mainFunction.basicBlocks; node <- block.nodes) {
      node match {
        case OutNode(id, valueVar, location) => {
          sb.append("Out('id" + id + "', 'v" + valueVar + "').\n");
        }

        case IfNode(id, valueVar, joinBlock, location) => {
          sb.append("Branch('id" + id + "', 'v" + valueVar + "').\n");
          if (!joinBlock.isEmpty) {
            sb.append("Join('id" + id + "', 'id" + joinBlock.nodes.head.id + "').\n");
          }
        }

        case IntegerLiteralNode(id, value, resultVar, high, location) => {
          sb.append("IntConst('id" + id + "', '" + value + "', 'v" + resultVar + "').\n");
          if (high) {
            sb.append("High('v" + resultVar + "').\n");
          }
        }

        case ObjectLiteralNode(id, resultVar, location) =>
          sb.append("ObjConst('id" + id + "', 'v" + resultVar + "').\n");

        case ReadVariableNode(id, name, resultVar, location) =>
          sb.append("AssignVariable('id" + id + "', '" + name + "', 'v" + resultVar + "').\n");

        case WriteVariableNode(id, name, valueVar, location) =>
          sb.append("AssignVariable('id" + id + "', 'v" + valueVar + "', '" + name + "').\n");

        case ReadPropertyNode(id, name, baseVar, resultVar, location) =>
          sb.append("ReadProperty('id" + id + "', 'v" + baseVar + "', '" + name + "', 'v" + resultVar + "').\n");

        case WritePropertyNode(id, name, baseVar, valueVar, location) =>
          sb.append("WriteProperty('id" + id + "', 'v" + baseVar + "', '" + name + "', 'v" + valueVar + "').\n");

        case _ => // ignored node
      }

    }

    for (block <- mainFunction.basicBlocks) {
      val nodes = block.nodes;
      var i = 0;
      for (i <- 1 to nodes.size - 1) {
        sb.append("Successor('id" + nodes(i - 1).id + "', 'id" + nodes(i).id + "').\n");
      }

      for (successor <- block.successors) {
        if (!block.isEmpty && !successor.isEmpty) {
          sb.append("Successor('id" + nodes.last.id + "', 'id" + successor.nodes.head.id + "').\n");
        }
      }
    }

    for (block <- mainFunction.basicBlocks) {
      if (!block.isEmpty) {
        val count = flowGraph.predecessorsOf(block).size;
        sb.append("CountPredecessors('id" + block.nodes.head.id + "', '" + count + "').\n");
        for (node <- block.nodes.drop(1)) {
          sb.append("CountPredecessors('id" + node.id + "', '1').\n");
        }
      }
    }

    sb.toString;
  }

}